Calculus of Construction

Lambda Cube

• different ways that terms (values) and types can depend on each other
• Calculus of Constructions sits at the apex of this cube
• Terms depending on terms:
  • : a function takes a value and returns a value.
  • the standard function application found in most programming languages
• Terms depending on types (Polymorphism):
  • : allows for the creation of functions that can operate on multiple types.
  • eg: a single length function that can determine the number of elements in a list of integers, a list of strings, or a list of any other type.
• Types depending on types (Type Operators):
  • : enables the creation of "functions for types."
  • eg: a generic List type constructor that can take any type T and produce a new type, List<T>
• Types depending on terms (Dependent Types):
  • : allows the type of a value to depend on another value
  • the most powerful feature
  • For instance, one can define a type for vectors that includes their length, such as Vector(n), where n is a natural number. This means a function that expects a Vector(3) cannot be accidentally given a Vector(4), and this correctness is guaranteed at the level of the type system
• Calculus of Construction provides all these forms of dependency